\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$, ${\it Out}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$), ${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)).\+
\\[0ex]chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\Rightarrow$ \=($\forall$$x$, $y$:Id.\+
\\[0ex]$x$ $<<$ $y$ $\Rightarrow$ ($\forall$$e$:E(${\it Sys}$). ($x$ $\in$ ${\it chain}$($e$)) $\Rightarrow$ ($y$ $\in$ ${\it chain}$($e$)) $\Rightarrow$ $x$ before $y$ $\in$ ${\it chain}$($e$))))
\-\-
\end{tabbing}